\def\cprime{$'$}
\begin{thebibliography}{10}

\bibitem{Ahrens2016}
Benedikt Ahrens.
\newblock Modules over relative monads for syntax and semantics.
\newblock {\em Math. Structures Comput. Sci.}, 26(1):3--37, 2016.

\bibitem{RezkCompletion}
Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman.
\newblock Univalent categories and the {R}ezk completion.
\newblock {\em Math. Structures Comput. Sci.}, 25(5):1010--1039, 2015.

\bibitem{ACU}
Thorsten Altenkirch, James Chapman, and Tarmo Uustalu.
\newblock Monads need not be endofunctors.
\newblock In {\em Foundations of software science and computational
  structures}, volume 6014 of {\em Lecture Notes in Comput. Sci.}, pages
  297--311. Springer, Berlin, 2010.

\bibitem{ACU2}
Thorsten Altenkirch, James Chapman, and Tarmo Uustalu.
\newblock Monads need not be endofunctors.
\newblock {\em Logical Methods in Computer Science}, 11(1:3):1--40, 2015.

\bibitem{Cartmell0}
John Cartmell.
\newblock Generalised algebraic theories and contextual categories.
\newblock {\em Ph.D. Thesis, Oxford University}, 1978.
\newblock \url{http://www.cs.ru.nl/~spitters/Cartmell.pdf}.

\bibitem{Cartmell1}
John Cartmell.
\newblock Generalised algebraic theories and contextual categories.
\newblock {\em Ann. Pure Appl. Logic}, 32(3):209--243, 1986.

\bibitem{FPT}
Marcelo Fiore, Gordon Plotkin, and Daniele Turi.
\newblock Abstract syntax and variable binding (extended abstract).
\newblock In {\em 14th {S}ymposium on {L}ogic in {C}omputer {S}cience
  ({T}rento, 1999)}, pages 193--202. IEEE Computer Soc., Los Alamitos, CA,
  1999.

\bibitem{GabZis}
P.~Gabriel and M.~Zisman.
\newblock {\em Calculus of fractions and homotopy theory}.
\newblock Ergebnisse der Mathematik und ihrer Grenzgebiete, Band 35.
  Springer-Verlag New York, Inc., New York, 1967.

\bibitem{HM2007}
Andr{\'e} Hirschowitz and Marco Maggesi.
\newblock Modules over monads and linearity.
\newblock In {\em Logic, language, information and computation}, volume 4576 of
  {\em Lecture Notes in Comput. Sci.}, pages 218--237. Springer, Berlin, 2007.

\bibitem{HM2008}
Andr{\'e} Hirschowitz and Marco Maggesi.
\newblock Higher order theories.
\newblock {\em \url{http://arxiv.org/abs/0704.2900}}, 2010.

\bibitem{KLV1}
Chris Kapulkin, Peter~LeFanu Lumsdaine, and Vladimir Voevodsky.
\newblock The simplicial model of univalent foundations.
\newblock {\em Available at \url{http://arxiv.org/abs/1211.2851}}, 2012, 2014.

\bibitem{MacLane}
S.~MacLane.
\newblock {\em Categories for the working mathematician}, volume~5 of {\em
  Graduate texts in {M}athematics}.
\newblock Springer-Verlag, 1971.

\bibitem{MLTT79}
Per Martin-L{\"o}f.
\newblock Constructive mathematics and computer programming.
\newblock In {\em Logic, methodology and philosophy of science, {VI}
  ({H}annover, 1979)}, volume 104 of {\em Stud. Logic Found. Math.}, pages
  153--175. North-Holland, Amsterdam, 1982.

\bibitem{Bibliopolis}
Per Martin-L{\"o}f.
\newblock {\em Intuitionistic type theory}, volume~1 of {\em Studies in Proof
  Theory. Lecture Notes}.
\newblock Bibliopolis, Naples, 1984.
\newblock Notes by Giovanni Sambin.

\bibitem{Streicher}
Thomas Streicher.
\newblock {\em Semantics of type theory}.
\newblock Progress in Theoretical Computer Science. Birkh\"auser Boston Inc.,
  Boston, MA, 1991.
\newblock Correctness, completeness and independence results, With a foreword
  by Martin Wirsing.

\bibitem{NTS}
Vladimir Voevodsky.
\newblock Notes on type systems.
\newblock 2009--2012.
\newblock \url{https://github.com/vladimirias/old_notes_on_type_systems}.

\bibitem{CMUtalk}
Vladimir Voevodsky.
\newblock The equivalence axiom and univalent models of type theory.
\newblock {\em arXiv 1402.5556}, pages 1--11, 2010.
\newblock \url{http://arxiv.org/abs/1402.5556}.

\bibitem{Bsystems}
Vladimir Voevodsky.
\newblock B-systems.
\newblock {\em arXiv 1410.5389, submitted}, pages 1--17, 2014.

\bibitem{Cfromauniverse}
Vladimir Voevodsky.
\newblock A {C}-system defined by a universe category.
\newblock {\em Theory Appl. Categ.}, 30(37):1181--1215, 2015.
\newblock \url{http://www.tac.mta.ca/tac/volumes/30/37/30-37.pdf}.

\bibitem{UniMath2015}
Vladimir Voevodsky.
\newblock An experimental library of formalized mathematics based on the
  univalent foundations.
\newblock {\em Math. Structures Comput. Sci.}, 25(5):1278--1294, 2015.

\bibitem{LandC}
Vladimir Voevodsky.
\newblock Lawvere theories and {C-systems}.
\newblock {\em arXiv 1512.08104}, pages 1--15, 2015.

\bibitem{fromunivwithpaths}
Vladimir Voevodsky.
\newblock Martin-{L}of identity types in the {C}-systems defined by a universe
  category.
\newblock {\em arXiv 1505.06446, under review in Publication IHES}, pages
  1--51, 2015.

\bibitem{fromunivwithPi}
Vladimir Voevodsky.
\newblock Products of families of types in the {C-systems} defined by a
  universe category.
\newblock {\em arXiv 1503.07072}, pages 1--30, 2015.

\bibitem{LandJf}
Vladimir Voevodsky.
\newblock Lawvere theories and {Jf}-relative monads.
\newblock {\em arXiv 1601.02158}, pages 1--21, 2016.

\bibitem{Csubsystems}
Vladimir Voevodsky.
\newblock Subsystems and regular quotients of {C-systems}.
\newblock In {\em Conference on Mathematics and its Applications, (Kuwait City,
  2014)}, number 658 in Contemporary Mathematics, pages 127--137, 2016.

\bibitem{UniMath}
Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et~al.
\newblock {\em UniMath}: {Univalent} {Mathematics}.
\newblock Available at \url{https://github.com/UniMath}.

\end{thebibliography}